/*
 * Main.cpp
 *
 *  Created on: May 3, 2011
 *      Author: trungtq
 */

#include <stdio.h>
#include <iostream>
#include <set>

#include "Function.h"
#include "Term.h"
#include "Utils.h"
#include "Equation.h"
#include "FastCC.h"


using namespace std;

int main1(int argc, char** argv) {
    try {
/*
        FunctionSet funcSet;
        VariableSet varSet;
        vector<string> eqStrings;
        eqStrings.push_back("f(a)=g(b)");
        eqStrings.push_back("g(c)=h(f(c),g(a))");
        eqStrings.push_back("b=c");
        eqStrings.push_back("f(c)=g(a)");
        eqStrings.push_back("h(d,d)=g(b)");
        eqStrings.push_back("g(a)=d");
        cout << "Input equation string: \n";
        for (int i = 0; i < eqStrings.size(); i++)
            cout << "   " << eqStrings.at(i) << "\n";
        // convert to term
        vector<Equation> eqVector;
        for (int i = 0; i < eqStrings.size(); i++) {
            string s = eqStrings.at(i);
            Equation eq = Equation::parseString(s, &funcSet, &varSet);
            eqVector.push_back(eq);
        }
        // print
        if (funcSet.size() == 0)
            cout << "No function symbols: \n";
        else {
            cout << "List of function symbols: \n";
            for (FunctionSet::iterator pos = funcSet.begin(); pos != funcSet.end(); pos++) {
                Function func = *pos;
                cout << "   " << func.toString() << "\n";
            }
        }

        if (varSet.size() == 0)
            cout << "No variables: \n";
        else {
            cout << "List of variables: \n";
            for (VariableSet::iterator pos = varSet.begin(); pos != varSet.end(); pos++) {
                Variable var = *pos;
                cout << "   " << var.toString() << "\n";
            }
        }

        cout << "List of equations: \n";
        for (vector<Equation>::iterator pos = eqVector.begin(); pos != eqVector.end(); pos++) {
            Equation eq = *pos;
            cout << "   " << eq.toString() << "\n";
        }

        // currify
        vector<Equation> currifiedEqs;
        for (vector<Equation>::iterator pos = eqVector.begin(); pos != eqVector.end(); pos++) {
            Equation eq = *pos;
            Equation ceq = Utils::currify(eq);
            currifiedEqs.push_back(ceq);
        }

        cout << "List of currified equations: \n";
        for (vector<Equation>::iterator pos = currifiedEqs.begin(); pos != currifiedEqs.end(); pos++) {
            Equation eq = *pos;
            cout << "   " << eq.toString() << "\n";
        }

        // flatten
        TermMap flattenMap;
        TermSet flattenerSet;
        vector<Equation> flattenedEqs;
        for (vector<Equation>::iterator pos = currifiedEqs.begin(); pos != currifiedEqs.end(); pos++) {
            Equation ceq = *pos;
            Equation feq = Utils::flatten(ceq, &flattenMap, &flattenerSet);
            flattenedEqs.push_back(feq);
        }
        cout << "List of flattened equations (before): \n";
        for (vector<Equation>::iterator pos = flattenedEqs.begin(); pos != flattenedEqs.end(); pos++) {
            Equation eq = *pos;
            cout << "   " << eq.toString() << "\n";
        }
        for (TermMap::iterator pos = flattenMap.begin(); pos != flattenMap.end(); pos++ ){
            Term term = pos->first;
            if (!Utils::isFlattener(term)) {
                Term flattenedTerm = pos->second;
                Equation newEq = Equation(term, flattenedTerm);
                flattenedEqs.push_back(newEq);
            }
        }
        cout << "List of flattened equations: \n";
        for (vector<Equation>::iterator pos = flattenedEqs.begin(); pos != flattenedEqs.end(); pos++) {
            Equation eq = *pos;
            cout << "   " << eq.toString() << "\n";
        }
        cout << "List of flattener: \n";
        for (TermSet::iterator pos = flattenerSet.begin(); pos != flattenerSet.end(); pos++) {
            Term term = *pos;
            cout << "   " << term.toString() << "\n";
        }
        // initialize fastCC
        FastCC fastCC = FastCC();
        fastCC.initialize(funcSet, varSet, flattenerSet);
        // merge
        for (vector<Equation>::iterator pos = flattenedEqs.begin(); pos != flattenedEqs.end(); pos++) {
            Equation eq = *pos;
            fastCC.merge(eq);
        }
        cout << "List of class: \n";
        ClassList classList = fastCC.getAllClassLists();
        for (ClassList::iterator pos = classList.begin(); pos != classList.end(); pos++) {
            Term representative = pos->first;
            TermList termList = pos->second;
            cout << "  " << representative.toString() << "  --->  { ";
            for (TermList::iterator loc = termList.begin(); loc != termList.end(); loc++) {
                Term term = *loc;
                cout << term.toString() << "; ";
            }
            cout << "}\n";
        }
        */
//
//        FastCC otherFastCC = FastCC();
//        otherFastCC.initialize(funcSet, varSet, flattenerSet);
//        // merge
//        for (vector<Equation>::iterator pos = flattenedEqs.begin(); pos != flattenedEqs.end(); pos++) {
//            Equation eq = *pos;
//            otherFastCC.merge(eq);
//        }
//        cout << "Other FassCC - List of class: \n";
//        ClassList otherClassList = otherFastCC.getAllClassLists();
//        for (ClassList::iterator pos = otherClassList.begin(); pos != otherClassList.end(); pos++) {
//            Term representative = pos->first;
//            TermList termList = pos->second;
//            cout << "  " << representative.toString() << "  --->  { ";
//            for (TermList::iterator loc = termList.begin(); loc != termList.end(); loc++) {
//                Term term = *loc;
//                cout << term.toString() << "; ";
//            }
//            cout << "}\n";
//        }

        FunctionSet funcSet;
        VariableSet varSet;
        vector<string> eqStrings;
        eqStrings.push_back("f(a)=g(b)");
        eqStrings.push_back("g(c)=h(f(c),g(a))");
        eqStrings.push_back("b=c");
        eqStrings.push_back("f(c)=g(a)");
        eqStrings.push_back("h(d,d)=g(b)");
        eqStrings.push_back("g(a)=d");
        cout << "Input equation string: \n";
        for (int i = 0; i < eqStrings.size(); i++)
            cout << "   " << eqStrings.at(i) << "\n";
        FastCC fastCC;
        fastCC.findCC(eqStrings);

        fastCC.printLookupTable();
        fastCC.printFlattenMap();

        Term t = Term::parseString(string("h(d,d)"));
        Term n_t = fastCC.normalize(t);
        Term no_t;
        //= fastCC.otherNormalize(t);
//        cout << "  " << t.toString() << "  -->  " << n_t.toString() << "  -->  " << no_t.toString() << "\n";
        t = Term::parseString(string("g(c)"));
        n_t = fastCC.normalize(t);
        cout << "  " << t.toString() << "  -->  " << n_t.toString() << "\n";
        t = Term::parseString(string("f(c)"));
        n_t = fastCC.normalize(t);
        cout << "  " << t.toString() << "  -->  " << n_t.toString() << "\n";
        t = Term::parseString(string("g(a)"));
        n_t = fastCC.normalize(t);
        cout << "  " << t.toString() << "  -->  " << n_t.toString() << "\n";
        t = Term::parseString(string("h(f(c),g(a))"));
        n_t = fastCC.normalize(t);
//        t = Term::parseString(string(".(E5,E6)"));
        no_t = fastCC.otherNormalize(t);
        cout << "  " << t.toString() << "  -->  " << n_t.toString() << "  -->  " << no_t.toString() << "\n";
    } catch (CCException e) {
        e.report();
    }
    return 1;
}
